RngSig{i}  RngSig{[i | j]} 

latex

Up	rings 1
Definitions of Statement	RngSig
Definitions	t  T, x:A. B(x), RngSig, S  T
Lemmas	unit wf, bool wf